(set-logic QF_BV)
(declare-fun x () (_ BitVec 2))
(declare-fun y () (_ BitVec 2))
(declare-fun z () (_ BitVec 1))
(declare-fun b () Bool)
(assert 
  (let ((e7 ((_ repeat 1) x))) 
  (let ((e10 (ite (bvslt y (_ bv0 2)) (_ bv1 1) (_ bv0 1)))) 
  (let ((e19 (ite (= e7 (_ bv0 2)) (_ bv1 1) (_ bv0 1)))) 
  (let ((e20 (ite b (_ bv0 1) z))) 
  (let ((e23 (ite (bvslt e10 z) (_ bv1 1) (_ bv0 1)))) 
  (let ((e35 (ite (= z (_ bv0 1)) (_ bv1 1) (_ bv0 1)))) 
  (let ((e36 (bvsge (_ bv0 2) ((_ zero_extend 1) e19)))) 
  (let ((e43 (bvslt e20 (_ bv0 1)))) 
  (let ((e55 (bvslt y (_ bv0 2)))) 
  (let ((e68 (distinct (_ bv0 2) ((_ sign_extend 1) e23)))) 
  (let ((e79 (bvuge (_ bv0 2) x))) 
  (let ((e97 (bvult (_ bv0 1) e35))) 
  (let ((e40 (= ((_ zero_extend 1) e19) x))) 
  (let ((e134 (not e40)))
  (let ((e137 (xor e55 e68))) 
  (let ((e139 (not e36))) 
  (let ((e144 (ite e97 e139 e79))) 
  (let ((e47 (not e137))) 
  (let ((e48 e43)) 
  (let ((e173 (= e144 e48))) 
  (let ((e174 e173)) 
  (let ((e177 (=> e134 e174))) 
  (let ((e180 e47)) 
  (let ((e184 (=> e180 e177))) 
  (let ((e202 e184)) e202))))))))))))))))))))))))))
(check-sat)

